[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification bin-min-heap-prepost
enrich
   bin-min-heap-inv

with
   

   
   
   functions  keyset : binheap → set;
   predicates  bin-heap-inv : binheap × array;
               bubble-up-inv : nat × binheap × array × binheap × array;
               bubble-down-inv : nat × binheap × array × binheap × array;
   
   
   
   

   

   axioms bin-heap-inv-def
          : ⊦   bin-heap-inv(bh, ar)
              ↔   bh.size ≤ # bh.ar ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ 2exp-size(# bh.ar)
                ∧ heap-order(bh.ar, bh.size);
          used for: ls;
          keyset :  ⊦ keyset(bh) = keyset(bh.ar, bh.size);
          used for: ls;
          bubble-up-inv
          : ⊦   bubble-up-inv(n, bh, ar, bh0, ar0)
              ↔   n < bh.size ∧ bh.size ≤ # bh.ar ∧ # bh.ar = # bh0.ar ∧ bh.size = bh0.size ∧ id-idx(ar0, ar)
                ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size)
                ∧ (n = 0 ∨ ¬ bh.ar[n].key < bh.ar[(n - 1) / 2].key → heap-order(bh.ar, bh.size))
                ∧ (n ≠ 0 ∧ bh.ar[n].key < bh.ar[(n - 1) / 2].key → heap-order(bh.ar[n, bh.ar[(n - 1) / 2]], bh.size))
                ∧ keyset(bh.ar, bh.size) = keyset(bh0.ar, bh0.size);
          used for: ls;
          bubble-down-inv
          : ⊦   bubble-down-inv(n, bh, ar, bh0, ar0)
              ↔   bh.size ≤ # bh.ar ∧ # bh.ar = # bh0.ar ∧ bh.size = bh0.size ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size)
                ∧ valid-idx(bh.ar, ar, bh.size)
                ∧ (    (2 * n + 1 < bh.size → ¬ bh.ar[2 * n + 1].key < bh.ar[n].key)
                     ∧ (2 * n + 2 < bh.size → ¬ bh.ar[2 * n + 2].key < bh.ar[n].key)
                   → heap-order(bh.ar, bh.size))
                ∧ (  2 * n + 1 < bh.size ∧ bh.ar[2 * n + 1].key < bh.ar[n].key ∨ 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[n].key
                   → heap-order
                     (bh.ar[n, (2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[2 * n + 1].key ⊃ bh.ar[2 * n + 2];bh.ar[2 * n + 1])], bh.size))
                ∧ keyset(bh.ar, bh.size) = keyset(bh0.ar, bh0.size);
          used for: ls;

   

   
end enrich